(DEFPROP ALLFNS
 (NIL COUNT COUNTA FIXUP COMMON COMA COMB COMC OCCUR SCOPE SCOPEA SCOPEB FIXUP2)
VALUE)

(DEFPROP COUNT
 (LAMBDA (E1 E2) (COND ((EQUAL E1 E2) 1) ((ATOM E2) 0) (T (COUNTA E1 (CDR E2)))))
EXPR)

(DEFPROP COUNTA
 (LAMBDA (E U) (COND ((NULL U) 0) (T (PLUS (COUNT E (CAR U)) (COUNTA E (CDR U))))))
EXPR)

(DEFPROP FIXUP
 (LAMBDA(E)
  ((LAMBDA(Z)
    (COND ((NULL Z) E)
	  (T ((LAMBDA (W) (LIST (LIST (QUOTE LAMBDA) (LIST W) (FIXUP (SUBST W Z E))) Z)) (GENSYM)))))
   (COMMON E)))
EXPR)

(DEFPROP COMMON
 (LAMBDA (E) ((LAMBDA (W) (COND ((NULL W) NIL) (T (COMC (CAR W) E (CDR W))))) (COMA E E 1)))
EXPR)

(DEFPROP COMA
 (LAMBDA (E1 E2 N) ((LAMBDA (W) (COND ((GREATERP W N) (CONS E1 W)) (T (COMB (CDR E1) E2 N)))) (COUNT E1 E2)))
EXPR)

(DEFPROP COMB
 (LAMBDA(U E N)
  (COND	((OR (NULL U) (ATOM (CAR U))) NIL)
	(T ((LAMBDA (Z) (COND ((NULL Z) (COMB (CDR U) E N)) (T Z))) (COMA (CAR U) E N)))))
EXPR)

(DEFPROP COMC
 (LAMBDA (E1 E N) ((LAMBDA (W) (COND ((NULL W) E1) (T (COMC (CAR W) E (CDR W))))) (COMA E1 E (ADD1 N))))
EXPR)

(DEFPROP OCCUR
 (LAMBDA (E E1) (OR (EQUAL E E1) (AND (NOT (ATOM E1)) (OR (OCCUR E (CAR E1)) (OCCUR E (CDR E1))))))
EXPR)

(DEFPROP SCOPE
 (LAMBDA(E E1)
  (COND	((EQUAL E E1) E)
	((NOT (OCCUR E E1)) NIL)
	(T ((LAMBDA (W) (COND ((NULL W) E1) (T W))) (SCOPEA E (CDR E1))))))
EXPR)

(DEFPROP SCOPEA
 (LAMBDA (E U) ((LAMBDA (Z) (COND ((NULL Z) (SCOPEA E (CDR U))) (T (SCOPEB E (CDR U) Z)))) (SCOPE E (CAR U))))
EXPR)

(DEFPROP SCOPEB
 (LAMBDA(E U Z)
  (COND ((NULL U) Z) (T ((LAMBDA (W) (COND ((NULL W) (SCOPEB E (CDR U) Z)) (T NIL))) (SCOPE E (CAR U))))))
EXPR)

(DEFPROP FIXUP2
 (LAMBDA(E)
  ((LAMBDA(X)
    (COND ((NULL X) E)
	  (T
	   ((LAMBDA(Y SYM)
	     (FIXUP2 (SUBST (LIST (LIST (QUOTE LAMBDA) (LIST SYM) (FIXUP2 (SUBST SYM X Y))) X) Y E)))
	    (SCOPE X E)
	    (GENSYM)))))
   (COMMON E)))
EXPR)